s:LOSet, a, b:|s|. (a <s b)  (a = b)  (b <s a) 

latex

Up	sets 1
Definitions of Statement	DSet, QOSet, POSet{i}, LOSet
Definitions	t  T, x:A. B(x), x,y. t(x;y), , P  Q, DSet, QOSet, POSet{i}, LOSet, P & Q, {T}, P  Q, x(s1,s2), P  Q, P  Q, Symmetrize(x,y.R(x;y);a;b)
Lemmas	loset wf, set car wf, loset properties, decidable set leq, set leq wf, connex iff trichot, set lt wf, set lt is sp of leq, poset anti sym